\begin{tabbing}
$\forall$${\it es}$:ES, $i$, $x$, $y$, $z$:Id, ${\it Tx}$, ${\it Ty}$, ${\it Tz}$:Type, $P$:(${\it Tx}$$\rightarrow$${\it Ty}$$\rightarrow$${\it Tz}$$\rightarrow$Prop), ${\it Lx}$, ${\it Ly}$, ${\it Lz}$:Knd List.
\\[0ex]es{-}frame(${\it es}$;$i$;${\it Lx}$;$x$;${\it Tx}$)
\\[0ex]$\Rightarrow$ es{-}frame(${\it es}$;$i$;${\it Ly}$;$y$;${\it Ty}$)
\\[0ex]$\Rightarrow$ es{-}frame(${\it es}$;$i$;${\it Lz}$;$z$;${\it Tz}$)
\\[0ex]$\Rightarrow$ \=$\forall$$e$@$i$.\+
\\[0ex](kind($e$) $\in$ ${\it Lx}$ @ ${\it Ly}$ @ ${\it Lz}$)
\\[0ex]$\Rightarrow$ $P$($x$ when $e$,$y$ when $e$,$z$ when $e$)
\\[0ex]$\Rightarrow$ $P$(($x$ after $e$),($y$ after $e$),($z$ after $e$))
\-\\[0ex]$\Rightarrow$ @$i$ stable ${\it state}$.$P$(${\it state}$.$x$,${\it state}$.$y$,${\it state}$.$z$)  
\end{tabbing}